package model.juliStaff.propo;

/*

    This file is part of Logica-Logike.

    Logica-Logike is free software: you can redistribute it and/or modify
    it under the terms of the GNU Lesser General Public License as published by
    the Free Software Foundation version 3 of the License.

    Logica-Logike is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU Lesser General Public License for more details.

    You should have received a copy of the GNU Lesser General Public License
    along with Logica-Logike.  If not, see <http://www.gnu.org/licenses/>.

 */
/**
 * Date: Sep 27, 2009 Time: 2:25:53 PM
 *
 * @author Maria Julia Racca;
 */

public class LogicalRules {

    public static MolecularProposition conjuncion(Proposition first,
                                                  Proposition second) {
        return new MolecularProposition(first, Operation.AND, second, false);
    }

    public static MolecularProposition adicion(Proposition p, Proposition add) {
        return new MolecularProposition(p, Operation.OR, add, false);
    }

    public static Proposition simplificacion(Proposition f, Proposition s) {
        return f;
        // o s!
    }

    public static Proposition SD(MolecularProposition f, Proposition p) {

        MolecularProposition mp = transform2(f);

        boolean error = mp.getFirst().compareTo(p) <= 0
                && mp.getSecond().compareTo(p) <= 0;
        if (error || !mp.getOperation().equals(Operation.OR)) {
            System.err.println("No se puede usar la regla SD");
            return null;
        }

        Proposition equal = null;
        Proposition notEqual = null;

        if (mp.getFirst().equals(p)) {
            equal = mp.getFirst();
            notEqual = mp.getSecond();
        } else {
            equal = mp.getSecond();
            notEqual = mp.getFirst();
        }

        if (p.getNegated().equals(equal.getNegated())) {
            System.err.println("No se puede usar la regla SD");
            return null;
        }

        return notEqual;
    }

    public static Proposition MPP(MolecularProposition f, Proposition p) {

        MolecularProposition mp = transform(f);

        Proposition first = mp.getFirst();
        Proposition second = mp.getSecond();

        boolean error = !first.equals(p);
        if (error || !mp.getOperation().equals(Operation.ENTONCES)) {
            System.err.println("No se puede usar la regla MPP");
            return null;
        }

        if (!p.getNegated().equals(first.getNegated())) {
            System.err.println("No se puede usar la regla MPP");
            return null;
        }

        return second;
    }

    public static Proposition MTT(MolecularProposition f, Proposition p) {

        MolecularProposition mp = transform(f);

        Proposition first = mp.getFirst();
        Proposition second = mp.getSecond();

        boolean error = second.compareTo(p) <= 0;
        if (error || !mp.getOperation().equals(Operation.ENTONCES)) {
            System.err.println("No se puede usar la regla MTT");
            return null;
        }

        if (p.getNegated().equals(second.getNegated())) {
            System.err.println("No se puede usar la regla MTT");
            return null;
        }

        first.setNegation(true);
        return first;
    }

    public static MolecularProposition SH(MolecularProposition f,
                                          MolecularProposition s) {

        MolecularProposition firstmp = transform(f);
        MolecularProposition secondmp = transform(s);

        Proposition first = firstmp.getFirst();
        Proposition second = firstmp.getSecond();
        Proposition third = secondmp.getSecond();

        boolean error = !second.equals(secondmp.getSecond());
        boolean error2 = !firstmp.getOperation().equals(Operation.ENTONCES)
                || !secondmp.getOperation().equals(Operation.ENTONCES);

        if (error || error2) {
            System.err.println("No se puede usar la regla MTT");
            return null;
        }

        return new MolecularProposition(first, Operation.ENTONCES, third, false);
    }

    public static MolecularProposition DC(MolecularProposition f,
                                          MolecularProposition s, MolecularProposition t) {

        MolecularProposition firstmp = transform(f);
        MolecularProposition secondmp = transform(s);
        MolecularProposition thirdmp = transform2(t);

        Proposition a = firstmp.getFirst();
        Proposition b = firstmp.getSecond();

        Proposition c = secondmp.getFirst();
        Proposition d = secondmp.getSecond();

        boolean error1 = !a.equals(thirdmp.getSecond())
                || !a.equals(thirdmp.getFirst());

        boolean error2 = !c.equals(thirdmp.getSecond())
                || !c.equals(thirdmp.getFirst());

        boolean error3 = !firstmp.getOperation().equals(Operation.ENTONCES)
                || !secondmp.getOperation().equals(Operation.ENTONCES)
                || !thirdmp.getOperation().equals(Operation.OR);

        if (error1 || error3 || error2) {
            System.err.println("No se puede usar la regla DC");
            return null;
        }

        return new MolecularProposition(b, Operation.OR, d, false);
    }

    public static MolecularProposition DD(MolecularProposition f,
                                          MolecularProposition s, MolecularProposition t) {

        MolecularProposition firstmp = transform(f);
        MolecularProposition secondmp = transform(s);
        MolecularProposition thirdmp = transform2(t);

        Proposition a = firstmp.getFirst();
        Proposition b = firstmp.getSecond();

        Proposition c = secondmp.getFirst();
        Proposition d = secondmp.getSecond();

        boolean error1 = b.compareTo(thirdmp.getSecond()) <= 0
                || b.compareTo(thirdmp.getFirst()) <= 0;

        boolean error2 = d.compareTo(thirdmp.getSecond()) <= 0
                || d.compareTo(thirdmp.getFirst()) <= 0;

        boolean error3 = !firstmp.getOperation().equals(Operation.ENTONCES)
                || !secondmp.getOperation().equals(Operation.ENTONCES)
                || !thirdmp.getOperation().equals(Operation.OR);

        if (error1 || error3 || error2) {
            System.err.println("No se puede usar la regla DD");
            return null;
        }

        a.setNegation(true);
        c.setNegation(true);

        return new MolecularProposition(a, Operation.OR, c, false);
    }

    private static MolecularProposition transform2(MolecularProposition t) {

        if (t.getNegated().equals(Operation.NOT)) {
            t = (MolecularProposition) LogicalLaws.leyDeMorgan(t);
        }

        return t;
    }

    private static MolecularProposition transform(MolecularProposition p) {

        if (p.getNegated().equals(Operation.NOT)) {
            p = (MolecularProposition) LogicalLaws
                    .definicionCondicional(LogicalLaws.leyDeMorgan(p));
        }

        return p;
    }

    public static boolean checkRule(Proposition f, Proposition s,
                                    Proposition t, LogicalRulesEnum rule, Proposition fin) {

        Proposition real = null;

        switch (rule) {

            case ADICION:
                real = adicion(f, s);
                break;
            case CONJUNCION:
                real = conjuncion(f, s);
                break;
            case DC:
                real = DC((MolecularProposition) f, (MolecularProposition) s,
                        (MolecularProposition) t);
                break;
            case DD:
                real = DD((MolecularProposition) f, (MolecularProposition) s,
                        (MolecularProposition) t);
                break;
            case MPP:
                real = MPP((MolecularProposition) f, s);
                break;
            case MTT:
                real = MTT((MolecularProposition) f, s);
                break;
            case SD:
                real = SD((MolecularProposition) f, s);
                break;
            case SH:
                real = SH((MolecularProposition) f, (MolecularProposition) s);
                break;
            case SIMPLIFICACION:
                real = simplificacion(f, s);
                break;
            default:
                break;
        }

        return fin != null && fin.equals(real);

    }

}
